\begin{tabbing}
($\backslash$p\=.let i = mvt (var\_of\_hyp ({-}2) p) in \+
\\[0ex]let ip1 = mk\_add\_term  i 1 in 
\\[0ex]((DTerm ip1 (
\-\\[0ex]{-}\=1)) \+
\\[0ex]CollapseTHENM (DTerm i ({-}1)))$\cdot$ p)
\-
\end{tabbing}